msg{-}item(${\it ds}$;${\it da}$;$k$;$l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it tg}$:Id$\times\mathbb{N}\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(fpf{-}cap(${\it da}$;KindDeq;rcv($l$,${\it tg}$);Void) List))